1. Field of the Invention
This invention relates to enhanced structural redundancy detection, and particularly to sequential redundancy identification algorithms for identifying gates within a sequential netlist.
2. Description of Background
Sequential redundancy identification algorithms have widespread applications, such as being the core techniques for sequential equivalence checking, and being critical to sequential design optimization techniques (for synthesis purposes).
A variety of techniques have been proposed for sequential redundancy identification. For example, one approach consists of first assuming all gates to be sequentially redundant, then performing an inductive fixed-point computation of iteratively forming smaller “buckets” of suspected-redundant pairs based upon failed equivalence-checking proofs. As another example, structural isomorphism approaches may be employed to attempt to identify gates, which must be sequentially redundant because of the structure of their cones of influence.
For instance, if gates g1 . . . gn in the logic cones upon which gates h1 and h2 are constructed may be correlated 1:1 such that only gates of identical function are mapped to each other; gates gi and gj are correlated only if all of their inputs are correlated; and inputs in the cone of h1 and h2 can only be reflexively mapped, then it is assured that h1 and h2 are sequentially redundant. Isomorphism-based redundancy detection is lossy, in that two gates, which behave redundantly, may not have isomorphic cones. Nonetheless, isomorphism-based redundancy detection may be much faster than traditional semantic-analysis approaches.
A variety of techniques have been proposed for sequential redundancy identification. However, existing sequential redundancy identification techniques are slow and not scalable. It is desired to provide sequential identification techniques to advance the speed and scalability of sequential redundancy identification.